In the following posts, we adress the proof of an upper bound on the Ramsey numbers. Ultimately, we want to arrive at the result that the \(k\)-th Ramsey number is bounded above by \(2^{2k-3}\). In this first post, we will introduce the required definitions and prove the prerequisites required for the main result.

Definition of Ramsey property

Before defining the Ramsey numbers, the book introduces the so-called “Ramsey property” of a complete graph.

Ramsey property. Consider the complete graph \(K_N\) on \(N\) vertices. We say that \(K_N\) has property \((m, n)\) if, no matter how we color the edges of \(K_N\) red and blue, there is always a complete subgraph on \(m\) vertices with all edges colored red or a complete subgraph on n vertices with all edges colored blue.
Aigner, M., & Ziegler, G. M. (5th ed.). Proofs from THE BOOK, p. 296.

We will already diverge from the literal definition in our implementation, because that will make our lives much easier: Since the theorem is only about two-colorings of the complete graph \(K_N\), we don’t need to actually use a data structure assigning colors to graph edges explicitly. Instead, we can represent the set of colorings in questions as the set of graphs \(C\) on \(N\) vertices, and consider an edge \((v, w)\) to be colored blue in \(K_N\) if the vertices \(v\) and \(w\) are adjacent in \(C\), and red if they are nonadjacent. This allows us to use the machinery for cliques and independent sets when talking about the Ramsey property, since our definition translates to the following:

Ramsey property, adjacency version. We say that \(K_N\) has property \((m, n)\) if, no matter which graph \(C\) on \(N\) vertices we choose, there is always an independent set of \(m\) vertices or a clique of n vertices.

This does not translate to Lean literally, since “a graph on \(N\) vertices” is not a builtin type. Instead, we need to quantify over the vertex types that are finite with N elements. This sorted, we can write down our definition!

1
2
3
4

def ramseyProp (N m n : ℕ) :=
    ∀ (V : Type) [Fintype V] [DecidableEq V] (_ : Fintype.card V = N)
      (C : SimpleGraph V) [DecidableRel C.Adj],
    ∃ (s : Finset V), (C.IsNIndepSet m s) ∨ (C.IsNClique n s)

Before we continue, let us introduce notation for subgraphs induces by vertex subsets:

1

notation:max G "[" A "]" => SimpleGraph.Subgraph.induce (⊤ : Subgraph G) (Finset.toSet A)

Definition of Ramsey number

A statement about monotonicity of this property follows:

Lemma. It is clear that if \(K_N\) has property \((m, n)\), then so does every \(K_s\) with \(s ≥ N\).
Aigner, M., & Ziegler, G. M. (5th ed.). Proofs from THE BOOK, p. 296. 
1
2

lemma ramseyProp_mono {m n : ℕ} (N s : ℕ) (h : N ≤ s) (ramseyProp_N : ramseyProp N m n) :
    ramseyProp s m n := by

The proof is omitted in the book, but we spell it out. First, we pick any N-element subset of the vertex set W of our s-graph, and consider the subgraph induced by it.

1
2
3
4

  intros W _ _ Wcard C _
  rw [← Wcard, ← Fintype.card_fin N] at h
  obtain ⟨A, A_subset, A_card⟩ := exists_subset_card_eq h
  let C' := C[A]

Since \(K_N\) has the Ramsey property, we can find a monochromatic vertex subset A' in the induced subgraph.

1

    obtain ⟨A', red_or_blue⟩ := ramseyProp_N A (by simp [A_card]) C'.coe

We embed A' back into W.

1

  use map ⟨Subtype.val, Subtype.val_injective⟩ A'

Since cliques and independent sets in the induced subgraph are also cliques and independent sets in the supergraph, the Ramsey property of the supergraph directly follows with the embedding of A' being monochromatic.

1

  exact Or.imp (induce_isNIndepSet C).mp (induce_isNClique C) red_or_blue

With this settled, we move on to actually defining the Ramsey number:

Ramsey number. (...) we ask for the smallest number \(N\) (if it exists) with this property — and this is the Ramsey number \(R(m, n)\).
Aigner, M., & Ziegler, G. M. (5th ed.). Proofs from THE BOOK, p. 296.

We use the sInf instance of Nat to talk about the smallest number of a set. It is noteworthy that this definition is zero if the set is empty, so the Lean definition does not quite match the paper one – existence of a graph with this property is not a prerequisite.

1
2
3
4

noncomputable def R (m n : ℕ) : ℕ := sInf { N | ramseyProp N m n}

notation:max "R(" m "," n ")" => R m n
notation:max "R(" n ")" => R n n

Note that we need to mark this definition as noncomputable, since finding the minimum of a set requires the set to be non-empty, and we have not yet established the existence of the Ramsey number for all m and n (in fact, this will be the largest effort of this entire proof). We could condition the definition on the existence of a Ramsey number and explicitly pass a proof. For the sake of brevity and since computability is not of the essence here, we will make this concession and profit from the nice results the mathlib already containsabout sInf.

Lemma for induction base case \(R(m, 2) = m\)

Let us establish the inductive principle that will be used to prove the main result, see also the previous post on induction in Lean.

Lemma. As a start, we certainly have \(R(m, 2) = m\) because either all of the edges of \(K_m\) are red or there is a blue edge, resulting in a blue \(K_2\).
Aigner, M., & Ziegler, G. M. (5th ed.). Proofs from THE BOOK, p. 296.

To this end, we will have to first prove that \(K_m\) actually has the \((m,2)\)-property, and then go on to prove that \(K_m\) is actually the smallest graph with this property. The first proof follows the book closely:

1
2
3

lemma ramseyProp_two {m : ℕ} : ramseyProp m m 2 := by
    intro _ _ _ cardV C _
    by_cases all_red : C.IsNIndepSet m univ

In the first case, all edges are red, so we’re done.

1

    · exact ⟨univ, (Or.inr all_red).symm⟩

In the second case, there is a blue edge, resulting in a blue \(K_2\).

1
2
3

    · simp [isNIndepSet_iff, isIndepSet_iff, Set.Pairwise, card_univ, cardV] at all_red
      obtain ⟨v, ⟨w, ⟨_, vwblue⟩⟩⟩ := all_red
      exact ⟨{v, w}, by simp_all [isNClique_iff]⟩

We can now prove the actual statement:

1

lemma ind_start_R_two {m : ℕ} : R(m, 2) = m := by

We bound the infimum by \(m\) from above and below. The bound from below follows by considering an all-red \(K_N\), in our representation the graph on \(N\) vertices with no edges ⊥, which has an \(N\)-independent set.

1
2
3
4
5

  have m_le_N (N : ℕ) (ram : ramseyProp N m 2) : m ≤ N := by
    obtain ⟨s, h⟩ := ram (Fin N) (Fintype.card_fin N) ⊥
    simp [isNClique_bot_iff] at h
    rw [← h.2]
    exact (card_finset_fin_le s)

The bound from above directly follows from the previous lemma, and we complete the proof.

1
2

  have r2 : ramseyProp m m 2 := ramseyProp_two
  exact le_antisymm (Nat.sInf_le r2) (le_csInf ⟨m, r2⟩ m_le_N)

Lemma for symmetry and induction base case

The other base case follows with symmetry, so we first need to establish that.

Lemma. By symmetry, we have \(R(2, m) = m\).
Aigner, M., & Ziegler, G. M. (5th ed.). Proofs from THE BOOK, p. 296.

We start off showing symmetry for the Ramsey property.

1
2

lemma ramseyProp_symm (m n N : ℕ) (h : ramseyProp N m n) :
    (ramseyProp N n m) := by

To this end, the hypothesis allows us to find a monochromatic subset in the complement graph.

1
2

  intro W _ _ Wcard C _
  obtain ⟨s, red_or_blue⟩ := h W Wcard Cᶜ

The result follows directly from the fact that a clique in a graph is an independent set in its complement and vice versa.

1
2
3

  cases' red_or_blue with c₁ c₂
  · exact ⟨s, Or.inr ((isNIndepSet_compl C).mp c₁)⟩
  · exact ⟨s, (Or.inr ((isNClique_compl C).mp c₂)).symm⟩

This easily transfers to the Ramsey number.

1
2
3

lemma R_symm {m n : ℕ} : R(m,n) = R(n,m) := by
  have {N : ℕ} := Iff.intro (ramseyProp_symm m n N) (ramseyProp_symm n m N)
  simp [R, this]

With this, we obtain our second base case:

1
2

lemma ind_start_two_R {m : ℕ} : R(2, m) = m := by
  simp[R_symm]; exact ind_start_R_two

Strict positivity

The proof for the recursive bound that we are going to attempt silently uses the fact that if both summands exist, \(N = R(m - 1, n) + R(m, n - 1)\) is strictly positive, i.e., non-zero, and so we can pick a vertex from \(K_N\). We show that the Ramsey number, if it exists, is positive if both \(m\) and \(n\) are strictly positive.

1
2

lemma R_pos (m n : ℕ) (_ : 0 < m) (_ : 0 < n) (h : ∃ N, ramseyProp N m n) :
    0 < R(m, n) := by

To this end, we assume \(0 = R(m, n)\):

1

  by_contra R0; apply Nat.eq_zero_of_not_pos at R0

Then zero has the ramsey property.

1

  have : ramseyProp 0 m n := R0 ▸ sInf_mem h

We can hence find \(s\), an \(m\)-independent set or an \(n\)-clique, in the empty graph.

1

  obtain ⟨s, p⟩ := this (Fin 0) rfl (⊥ : SimpleGraph (Fin 0))

That leads to contradiction, since \(s\) must be empty but \(0 < m,n\).

1
2
3

  simp_rw [isNIndepSet_iff, isNClique_iff,
    eq_zero_of_le_zero (card_finset_fin_le s)] at p
  cases p <;> simp_all

With these prerequisites in place, we are ready to tackle the recursive bound on Ramsey numbers in the next post.